i, j:Id. i = j  i = j 

latex

Definitions	i = j, x. t(x), eqof(d), IdDeq, t  T, Prop, b, x:A. B(x), P  Q, P & Q, P  Q, P  Q, Id
Lemmas	assert wf, id-deq wf, eqof wf, Id wf, deq property, iff functionality wrt iff, all functionality wrt iff